COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% These axioms reify goals and actions.  They enable us to prove
C00006 ENDMK
C⊗;
% These axioms reify goals and actions.  They enable us to prove
% should(I,prog(walk(car),drive(airport)),S0)

% Warning: These axioms haven't been checked to see that misguided subsitutions
% (e.g. using a situation as a person) can't give strange results.
% The axioms can be complicated by adding premisses to ensure that
% situations are never substituted for variables standing for persons,
% but the sort mechanism (which will be explained later) does it better.

declare INDVAR x y z s p a1 a2 g a;

declare INDCONST I, S0, desk, home,car,airport,county;

declare PREDCONST att 2, walkable 1, drivable 1;

declare PREDCONST holds 2, wants 3, should 3;

declare OPCONST at 2, result 3, prog 2, walk 1, drive 1;

axiom walkable:	walkable(home);;

axiom drivable:	drivable(county);;

axiom at:
	holds(at(I,desk),S0)
	att(desk,home)
	holds(at(car,home),S0)
	att(home,county)
	att(airport,county)
;;

axiom ats:	∀x y.(att(x,y) ⊃ ∀s.holds(at(x,y),s));;

axiom attrans:
	∀x y z s.(holds(at(x,y),s) ∧ holds(at(y,z),s) ⊃ holds(at(x,z),s))
	∀x y z.(att(x,y) ∧ att(y,z) ⊃ att(x,z))
;;

axiom notI:	¬(I=desk) ∧ ¬(I=car) ∧ ¬(I=home) ∧ ¬(I=airport);;

axiom walk:
	∀x y z p s.((walkable(x) ∧ (att(y,x)∨holds(at(y,x),s)) ∧ (att(z,x)
				∨ holds(at(z,x),s))
			 ∧ holds(at(p,y),s))
		⊃ (holds(at(p,z),result(p,walk(z),s))
		   ∧ ∀x y.(¬(x = I) 
		⊃ (holds(at(x,y),result(p,walk(z),s)) ≡ holds(at(x,y),s)))))
;;

axiom drive:
	∀x y z p s.((drivable(x) ∧ att(y,x) 
				∧ att(z,x) ∧ holds(at(car,y),s) 
					∧ holds(at(p,car),s))
		⊃ (holds(at(car,z),result(p,drive(z),s))
		∧ ∀x y.(¬(x = car ∨ holds(at(x,car),s)) ∨ y=car
			 ⊃ (holds(at(x,y),result(p,drive(z),s)) 
					≡ holds(at(x,y),s)))))
;;

axiom prog:
	∀a1 a2 p s.(result(p,prog(a1,a2),s) = result(p,a2,result(p,a1,s)))
;;

axiom should:
	∀p g a s.(wants(p,g,s) ∧ holds(g,result(p,a,s)) ⊃ should(p,a,s))
;;

axiom want:
	wants(I,at(I,airport),S0)
;;